$\forall$$T$:Type, $L$:($T$ List), $x$, $y$:$T$.
\\[0ex]no\_repeats($T$;$L$)
\\[0ex]$\Rightarrow$ adjacent($T$;$L$;$x$;$y$)
\\[0ex]$\Rightarrow$ ($\forall$$z$:$T$. $x$ before $z$ $\in$ $L$ $\Rightarrow$ ($y$ before $z$ $\in$ $L$ $\vee$ ($z$ = $y$)))